0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 16 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 17 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
transpose_in_gg(A, B) → U1_gg(A, B, transpose_aux_in_ggg(A, [], B))
transpose_aux_in_ggg(.(R, Rs), X1, .(C, Cs)) → U2_ggg(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
row2col_in_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
row2col_in_ggaa([], [], [], []) → row2col_out_ggaa([], [], [], [])
U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_ggaa(Xs, Cols, Cols1, As)) → row2col_out_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_ggg(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → U3_ggg(R, Rs, X1, C, Cs, transpose_aux_in_ggg(Rs, Accm, Cols1))
transpose_aux_in_ggg([], X, X) → transpose_aux_out_ggg([], X, X)
U3_ggg(R, Rs, X1, C, Cs, transpose_aux_out_ggg(Rs, Accm, Cols1)) → transpose_aux_out_ggg(.(R, Rs), X1, .(C, Cs))
U1_gg(A, B, transpose_aux_out_ggg(A, [], B)) → transpose_out_gg(A, B)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
transpose_in_gg(A, B) → U1_gg(A, B, transpose_aux_in_ggg(A, [], B))
transpose_aux_in_ggg(.(R, Rs), X1, .(C, Cs)) → U2_ggg(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
row2col_in_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
row2col_in_ggaa([], [], [], []) → row2col_out_ggaa([], [], [], [])
U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_ggaa(Xs, Cols, Cols1, As)) → row2col_out_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_ggg(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → U3_ggg(R, Rs, X1, C, Cs, transpose_aux_in_ggg(Rs, Accm, Cols1))
transpose_aux_in_ggg([], X, X) → transpose_aux_out_ggg([], X, X)
U3_ggg(R, Rs, X1, C, Cs, transpose_aux_out_ggg(Rs, Accm, Cols1)) → transpose_aux_out_ggg(.(R, Rs), X1, .(C, Cs))
U1_gg(A, B, transpose_aux_out_ggg(A, [], B)) → transpose_out_gg(A, B)
TRANSPOSE_IN_GG(A, B) → U1_GG(A, B, transpose_aux_in_ggg(A, [], B))
TRANSPOSE_IN_GG(A, B) → TRANSPOSE_AUX_IN_GGG(A, [], B)
TRANSPOSE_AUX_IN_GGG(.(R, Rs), X1, .(C, Cs)) → U2_GGG(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_IN_GGG(.(R, Rs), X1, .(C, Cs)) → ROW2COL_IN_GGAA(R, .(C, Cs), Cols1, Accm)
ROW2COL_IN_GGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_GGAA(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
ROW2COL_IN_GGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → ROW2COL_IN_GGAA(Xs, Cols, Cols1, As)
U2_GGG(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → U3_GGG(R, Rs, X1, C, Cs, transpose_aux_in_ggg(Rs, Accm, Cols1))
U2_GGG(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_GGG(Rs, Accm, Cols1)
transpose_in_gg(A, B) → U1_gg(A, B, transpose_aux_in_ggg(A, [], B))
transpose_aux_in_ggg(.(R, Rs), X1, .(C, Cs)) → U2_ggg(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
row2col_in_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
row2col_in_ggaa([], [], [], []) → row2col_out_ggaa([], [], [], [])
U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_ggaa(Xs, Cols, Cols1, As)) → row2col_out_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_ggg(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → U3_ggg(R, Rs, X1, C, Cs, transpose_aux_in_ggg(Rs, Accm, Cols1))
transpose_aux_in_ggg([], X, X) → transpose_aux_out_ggg([], X, X)
U3_ggg(R, Rs, X1, C, Cs, transpose_aux_out_ggg(Rs, Accm, Cols1)) → transpose_aux_out_ggg(.(R, Rs), X1, .(C, Cs))
U1_gg(A, B, transpose_aux_out_ggg(A, [], B)) → transpose_out_gg(A, B)
TRANSPOSE_IN_GG(A, B) → U1_GG(A, B, transpose_aux_in_ggg(A, [], B))
TRANSPOSE_IN_GG(A, B) → TRANSPOSE_AUX_IN_GGG(A, [], B)
TRANSPOSE_AUX_IN_GGG(.(R, Rs), X1, .(C, Cs)) → U2_GGG(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_IN_GGG(.(R, Rs), X1, .(C, Cs)) → ROW2COL_IN_GGAA(R, .(C, Cs), Cols1, Accm)
ROW2COL_IN_GGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_GGAA(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
ROW2COL_IN_GGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → ROW2COL_IN_GGAA(Xs, Cols, Cols1, As)
U2_GGG(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → U3_GGG(R, Rs, X1, C, Cs, transpose_aux_in_ggg(Rs, Accm, Cols1))
U2_GGG(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_GGG(Rs, Accm, Cols1)
transpose_in_gg(A, B) → U1_gg(A, B, transpose_aux_in_ggg(A, [], B))
transpose_aux_in_ggg(.(R, Rs), X1, .(C, Cs)) → U2_ggg(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
row2col_in_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
row2col_in_ggaa([], [], [], []) → row2col_out_ggaa([], [], [], [])
U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_ggaa(Xs, Cols, Cols1, As)) → row2col_out_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_ggg(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → U3_ggg(R, Rs, X1, C, Cs, transpose_aux_in_ggg(Rs, Accm, Cols1))
transpose_aux_in_ggg([], X, X) → transpose_aux_out_ggg([], X, X)
U3_ggg(R, Rs, X1, C, Cs, transpose_aux_out_ggg(Rs, Accm, Cols1)) → transpose_aux_out_ggg(.(R, Rs), X1, .(C, Cs))
U1_gg(A, B, transpose_aux_out_ggg(A, [], B)) → transpose_out_gg(A, B)
ROW2COL_IN_GGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → ROW2COL_IN_GGAA(Xs, Cols, Cols1, As)
transpose_in_gg(A, B) → U1_gg(A, B, transpose_aux_in_ggg(A, [], B))
transpose_aux_in_ggg(.(R, Rs), X1, .(C, Cs)) → U2_ggg(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
row2col_in_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
row2col_in_ggaa([], [], [], []) → row2col_out_ggaa([], [], [], [])
U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_ggaa(Xs, Cols, Cols1, As)) → row2col_out_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_ggg(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → U3_ggg(R, Rs, X1, C, Cs, transpose_aux_in_ggg(Rs, Accm, Cols1))
transpose_aux_in_ggg([], X, X) → transpose_aux_out_ggg([], X, X)
U3_ggg(R, Rs, X1, C, Cs, transpose_aux_out_ggg(Rs, Accm, Cols1)) → transpose_aux_out_ggg(.(R, Rs), X1, .(C, Cs))
U1_gg(A, B, transpose_aux_out_ggg(A, [], B)) → transpose_out_gg(A, B)
ROW2COL_IN_GGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → ROW2COL_IN_GGAA(Xs, Cols, Cols1, As)
ROW2COL_IN_GGAA(.(X, Xs), .(.(X, Ys), Cols)) → ROW2COL_IN_GGAA(Xs, Cols)
From the DPs we obtained the following set of size-change graphs:
U2_GGG(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_GGG(Rs, Accm, Cols1)
TRANSPOSE_AUX_IN_GGG(.(R, Rs), X1, .(C, Cs)) → U2_GGG(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
transpose_in_gg(A, B) → U1_gg(A, B, transpose_aux_in_ggg(A, [], B))
transpose_aux_in_ggg(.(R, Rs), X1, .(C, Cs)) → U2_ggg(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
row2col_in_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
row2col_in_ggaa([], [], [], []) → row2col_out_ggaa([], [], [], [])
U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_ggaa(Xs, Cols, Cols1, As)) → row2col_out_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_ggg(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → U3_ggg(R, Rs, X1, C, Cs, transpose_aux_in_ggg(Rs, Accm, Cols1))
transpose_aux_in_ggg([], X, X) → transpose_aux_out_ggg([], X, X)
U3_ggg(R, Rs, X1, C, Cs, transpose_aux_out_ggg(Rs, Accm, Cols1)) → transpose_aux_out_ggg(.(R, Rs), X1, .(C, Cs))
U1_gg(A, B, transpose_aux_out_ggg(A, [], B)) → transpose_out_gg(A, B)
U2_GGG(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_GGG(Rs, Accm, Cols1)
TRANSPOSE_AUX_IN_GGG(.(R, Rs), X1, .(C, Cs)) → U2_GGG(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs), Cols1, Accm))
row2col_in_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_ggaa(Xs, Cols, Cols1, As))
U4_ggaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_ggaa(Xs, Cols, Cols1, As)) → row2col_out_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
row2col_in_ggaa([], [], [], []) → row2col_out_ggaa([], [], [], [])
U2_GGG(R, Rs, X1, C, Cs, row2col_out_ggaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_GGG(Rs, Accm, Cols1)
TRANSPOSE_AUX_IN_GGG(.(R, Rs), X1, .(C, Cs)) → U2_GGG(R, Rs, X1, C, Cs, row2col_in_ggaa(R, .(C, Cs)))
row2col_in_ggaa(.(X, Xs), .(.(X, Ys), Cols)) → U4_ggaa(X, Xs, Ys, Cols, row2col_in_ggaa(Xs, Cols))
U4_ggaa(X, Xs, Ys, Cols, row2col_out_ggaa(Xs, Cols, Cols1, As)) → row2col_out_ggaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
row2col_in_ggaa([], []) → row2col_out_ggaa([], [], [], [])
row2col_in_ggaa(x0, x1)
U4_ggaa(x0, x1, x2, x3, x4)
From the DPs we obtained the following set of size-change graphs: